; COMMAND-LINE: --strings-exp --seq-array=lazy
; EXPECT: unknown
(set-logic ALL)
(declare-sort T@$ 0)
(declare-sort |T@[| 0)
(declare-sort T 0)
(declare-sort T@ 0)
(declare-datatypes ((@ 0)) ((($1 (l Int)))))
(declare-datatypes (($1 0)) ((($1 (v (Seq @))))))
(declare-datatypes ((@$ 0)) ((($1 (p $1)))))
(declare-datatypes ((M 0)) (((M (c T@)))))
(declare-datatypes ((E 0)) (((T))))
(declare-datatypes ((@M 0)) (((M (|#| T)))))
(declare-datatypes (($E 0)) ((($E (s |T@[|)))))
(declare-fun S (|T@[| T@$) @M)
(declare-fun S (T E) Int)
(declare-fun |1| () M)
(declare-fun S (T@ Int) @$)
(declare-fun $ () Int)
(declare-fun e () $E)
(declare-fun t () Bool)
(assert (not (=> (and (forall ((h T@$)) (and (forall ((v E)) (= 0 (S (|#| (S (s e) h)) T)))))) (< 0 (seq.len (v (p (S (c |1|) 1))))) (and t (= 0 (l (seq.nth (v (p (S (c |1|) 1))) $)))))))
(check-sat)
